/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import java.util.Iterator;

import alloy.util.Dbg;

/** Evaluates a Boolean formula with respect to a given assignment of Boolean variables.
    The forXXXX methods return BooleanFormula.FALSE or BooleanFormula.TRUE. */
class Eval_V extends GBF_V {

    /** Values of all Boolean variables.  {@link #_assignment}[0] unused. */
    private boolean[] _assignment;

  /**
   * Evaluator for evaluating BooleanFormula's that do not mention any boolean variables
   * (i.e. have only constants or switchable constants at the leaves).
   */
  static Eval_V sDefaultEval_V; // = new Eval_V(new boolean[]{});
  
  public static void initSingleton() {
	  sDefaultEval_V = new Eval_V(new boolean[]{});
  }

    Eval_V(boolean[] assignment_) {
        Dbg.chk(assignment_);
        this._assignment = assignment_;
    }

    Object forConst(GBF_Const g_const) { return g_const; }

    Object forLit(GBF_Lit g_lit) {
        int lit = g_lit.getLit();
        Dbg.chk(_assignment);
        if (Math.abs(lit) >= _assignment.length)
            throw new Error("lit: " + lit + " len: " + _assignment.length);
        return
            ((lit > 0  &&  _assignment[lit])  ||
             (lit < 0  && !_assignment[-lit])) ? BooleanFormula.TRUE() : BooleanFormula.FALSE();
    }

    Object forNot(GBF_Not g_not) {
        return ((BooleanFormula)g_not.expr.acceptVisitor(this)).not();
    }

    Object forAnd(GBF_And g_and) {
        BooleanFormula result = BooleanFormula.TRUE();
        for (int i=0; i<g_and.subexprs.length  &&  result==BooleanFormula.TRUE(); i++)
            result = result.and(((BooleanFormula)g_and.subexprs[i].acceptVisitor(this)));
        return result;
    }

    Object forOr(GBF_Or g_or) {
        BooleanFormula result = BooleanFormula.FALSE();
        for (int i=0; i<g_or.subexprs.length  &&  result==BooleanFormula.FALSE(); i++)
            result = result.or(((BooleanFormula)g_or.subexprs[i].acceptVisitor(this)));
        return result;
    }

    Object forVarConst(VarConst varConst_) {
        return BooleanFormula.makeConst((varConst_.var.getVarValue() &  (1L << varConst_.val))  >  0);
    }

    Object forSetVarExpr(SetVarExpr setVarExpr_) {
        setVarExpr_.var.setVarValue(setVarExpr_.val);
        Object result = setVarExpr_.expr.acceptVisitor(this);
        setVarExpr_.var.clearVarValue();
        return result;
    }

    Object forCNFFunc(CNFFunc cnfFunc_) {
        // determine the truth value of each child.  this
        // gives the truth value of all literals except for the
        // literal representing the result.
        BooleanFormula[] subs = cnfFunc_.subexprs;
        boolean[] subVals = new boolean[subs.length];
        for (int i=0; i<subs.length; i++) {
            BooleanFormula childVal = (BooleanFormula)subs[i].acceptVisitor(this);
            Dbg.chk(childVal == BooleanFormula.TRUE() ||
                childVal == BooleanFormula.FALSE());
            subVals[i] = (childVal == BooleanFormula.TRUE());
        }

        // now, since all variables except the result variable have values,
        // all literals except the result literal have values.
        // so each clause is either subsumed, or else is a unit clause in which
        // the result literal is the only unset literal.
        // (if some clause does not have the result literal in it and is not subsumed,
        // then the Boolean function is not defined for the given input combination.)
        for (Iterator clauseIter = cnfFunc_.clauses.iterator(); clauseIter.hasNext();) {
            int[] clause = (int[])clauseIter.next();
            boolean foundTrueLit = false;
            int resultLit = 0;

            for (int i=0; !foundTrueLit && i<clause.length; i++) {
                int lit = clause[i];
                int var = Math.abs(clause[i]);

                if (var == cnfFunc_.getResultVar())
                    resultLit = lit;
                else {
                    boolean varTrue = subVals[var - 1];
                    if ((lit > 0 && varTrue) || (lit < 0 && !varTrue))
                        foundTrueLit = true;
                }
            }

            if (!foundTrueLit) {
                Dbg.chk(resultLit != 0);
                return resultLit > 0 ? BooleanFormula.TRUE() : BooleanFormula.FALSE();
            }
        }

        // for (Iterator clauseIter = cnfFunc_.clauses.iterator(); clauseIter.hasNext();) {
        //     int[] clause = (int[])clauseIter.next();
        //     System.out.println("clause: " + Util.str(clause));
        // }
        // for (int i=0; i<subVals.length; i++)
        //     System.out.println("var " + (i+1) + " : " + (subVals[i] ? "T" : "F"));
        // System.out.println("this: " + cnfFunc_);
        // Dbg.fail("poorly defined CNFFunc");

        return BooleanFormula.TRUE();
    }
}  // class Eval_V

